import z3
from Crypto.Util.number import *


def enc(key):
    R = bytes_to_long(b"Welcome To PaluCTF!")
    MOD = 2 ** 418
    R = R ^ ((R - 60) >> 24)
    R = R ^ ((R - 60) << 88)
    R ^= key
    R = (-R * R * 2024) % MOD
    R = (R * key) % MOD
    return R


res = 0x2E441F765514CCA89173554726494D37E9FBE774B6F807BC5F6E71117530CE3D7DB5F70554C03CD9055F4E42969600904DF1F4DB8
s = z3.Solver()
key = z3.BitVec("key", 418)
s.add(enc(key) == res)
s.check()
m = s.model()
flag = long_to_bytes(m[key].as_long())
print(flag)
